ES0
== E:Type
== EqDecider(E)
== T:(IdIdType)
== V:(IdIdType)
== M:(IdLnkIdType)
== Top
== loc:(EId)
== kind:(EKnd)
== val:(e:Eeventtype(kind;loc;V;M;e))
== when:(x:Ide:ET(loc(e),x))
== after:(x:Ide:ET(loc(e),x))
== sends:(l:IdLnkE(Msg_sub(l;M) List))
== sender:({e:E| isrcv(kind(e)) }E)
== index:(e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||)
== first:(E)
== pred:({e':E| first(e') }E)
== causl:(EEProp)
== ESAxioms(E;T;M;
== ESAxioms(loc;kind;val;
== ESAxioms(when;after;
== ESAxioms(sends;sender;index;
== ESAxioms(first;pred;
== ESAxioms(causl)
== ESAtomAxiom{i:l}(T;i,k. kindcase(k; a.V(i,a); l,t.M(l,t) ))
== Top 

latex

---

clarification:

event-system0{i:l}
== E:Type{i}
== EqDecider(E)
== T:(IdIdType{i})
== V:(IdIdType{i})
== M:(IdLnkIdType{i})
== Top
== loc:(EId)
== kind:(EKnd)
== val:(e:Eeventtype(kind;loc;V;M;e))
== when:(x:Ide:ET(loc(e),x))
== after:(x:Ide:ET(loc(e),x))
== sends:(l:IdLnkE(Msg_sub(l;M) List))
== sender:({e:E| isrcv(kind(e)) }E)
== index:(e:{e:E| isrcv(kind(e)) }{0..||sends(lnk(kind(e)),sender(e))||})
== first:(E)
== pred:({e':E| first(e') }E)
== causl:(EEProp{i})
== ESAxioms{i:l}
== ESAxioms(E; T; M; loc; kind; val; when; after; sends; sender; index; first; pred; causl)
== ESAtomAxiom{i:l}
== ESAtomAxiom(T; (i,k. kindcase(k; a.V(i,a); l,t.M(l,t) )))
== Top 

latex

Definitions	EqDecider(T), Type, Knd, eventtype(k;loc;V;M;e), Id, IdLnk, type List, Msg_sub(l;M), isrcv(k), {i..j}, #$n, ||as||, lnk(k), , {x:A| B(x) }, A, b, x:AB(x), Prop, ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), x:AB(x), ESAtomAxiom{i:l}(T;V), x.A(x), kindcase(k; a.f(a); l,t.g(l;t) ), f(a), Top
FDL editor aliases	event-system0